The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

cond_scanr_f_z_xs_1(Cons(0, x11), 0) → Cons(0, Cons(0, x11))
cond_scanr_f_z_xs_1(Cons(S(x2), x11), 0) → Cons(S(x2), Cons(S(x2), x11))
cond_scanr_f_z_xs_1(Cons(0, x11), M(x2)) → Cons(0, Cons(0, x11))
cond_scanr_f_z_xs_1(Cons(S(x40), x23), M(0)) → Cons(S(x40), Cons(S(x40), x23))
cond_scanr_f_z_xs_1(Cons(S(x8), x23), M(S(x4))) → Cons(minus#2(x8, x4), Cons(S(x8), x23))
cond_scanr_f_z_xs_1(Cons(0, x11), S(x2)) → Cons(S(x2), Cons(0, x11))
cond_scanr_f_z_xs_1(Cons(S(x2), x11), S(x4)) → Cons(plus#2(S(x4), S(x2)), Cons(S(x2), x11))
scanr#3(Nil) → Cons(0, Nil)
scanr#3(Cons(x4, x2)) → cond_scanr_f_z_xs_1(scanr#3(x2), x4)
foldl#3(x2, Nil) → x2
foldl#3(x6, Cons(x4, x2)) → foldl#3(max#2(x6, x4), x2)
minus#2(0, x16) → 0
minus#2(S(x20), 0) → S(x20)
minus#2(S(x4), S(x2)) → minus#2(x4, x2)
plus#2(0, S(x2)) → S(x2)
plus#2(S(x4), S(x2)) → S(plus#2(x4, S(x2)))
max#2(0, x8) → x8
max#2(S(x12), 0) → S(x12)
max#2(S(x4), S(x2)) → S(max#2(x4, x2))
main(x1) → foldl#3(0, scanr#3(x1))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCpxRelTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to relative TRS where S is empty.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

cond_scanr_f_z_xs_1(Cons(0, x11), 0) → Cons(0, Cons(0, x11))
cond_scanr_f_z_xs_1(Cons(S(x2), x11), 0) → Cons(S(x2), Cons(S(x2), x11))
cond_scanr_f_z_xs_1(Cons(0, x11), M(x2)) → Cons(0, Cons(0, x11))
cond_scanr_f_z_xs_1(Cons(S(x40), x23), M(0)) → Cons(S(x40), Cons(S(x40), x23))
cond_scanr_f_z_xs_1(Cons(S(x8), x23), M(S(x4))) → Cons(minus#2(x8, x4), Cons(S(x8), x23))
cond_scanr_f_z_xs_1(Cons(0, x11), S(x2)) → Cons(S(x2), Cons(0, x11))
cond_scanr_f_z_xs_1(Cons(S(x2), x11), S(x4)) → Cons(plus#2(S(x4), S(x2)), Cons(S(x2), x11))
scanr#3(Nil) → Cons(0, Nil)
scanr#3(Cons(x4, x2)) → cond_scanr_f_z_xs_1(scanr#3(x2), x4)
foldl#3(x2, Nil) → x2
foldl#3(x6, Cons(x4, x2)) → foldl#3(max#2(x6, x4), x2)
minus#2(0, x16) → 0
minus#2(S(x20), 0) → S(x20)
minus#2(S(x4), S(x2)) → minus#2(x4, x2)
plus#2(0, S(x2)) → S(x2)
plus#2(S(x4), S(x2)) → S(plus#2(x4, S(x2)))
max#2(0, x8) → x8
max#2(S(x12), 0) → S(x12)
max#2(S(x4), S(x2)) → S(max#2(x4, x2))
main(x1) → foldl#3(0, scanr#3(x1))

S is empty.
Rewrite Strategy: INNERMOST

(3) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
scanr#3(Cons(x4, x2)) →⁺ cond_scanr_f_z_xs_1(scanr#3(x2), x4)
gives rise to a decreasing loop by considering the right hand sides subterm at position [0].
The pumping substitution is [x2 / Cons(x4, x2)].
The result substitution is [ ].

(4) BOUNDS(n^1, INF)